Beniamino Accattoli

Proof nets and the lambda-calculus 2.0

Abstract

The traditional proof nets representation of lambda-calculus dates back to the nineties, to the work of Danos and Regnier, and it is nowadays a cornerstone of the linear logic literature. In the last few years such a traditional view has been refined, building on a simple solution to its main issue, i.e. the different granularities of the evaluation mechanisms at work in the two systems. Such a solution, the linear substitution calculus, is both a refinement of lambda calculus and a graph-free presentation of proof nets. Its simplicity led to a new wave of studies on the topic, whose main achievement has been the development of a theory of cost models for the lambda calculus. The talk will be an introduction to the main ideas at work in the new framework, that are: an abstract point of view on proof nets, seen as a rewriting system up to a postponable structural equivalence, and not as a graphical language; a new, simpler presentation of linear head reduction, justified via rewriting and quantitative analyses; the extension of the theory to abstract machines and processes, them too seen as abstract proof nets evaluating via linear head reduction; the use of strong bisimulations to relate terms, graphs, machines, and processes in a perfect way. Beware: the talk will not be a bland survey of previous work, nor will it present recent results, in particular not those about cost models. It will rather be an original introduction to basic concepts, questioning the status quo, and stressing the change of perspective.